es:event_system{i:l}, e,e',a,b:es-E(es).
l_before(a; b; [e, e']; es-E(es))  (es-locl(es; a; b)  es-le(es; e; a)  es-le(es; b; e')) 

latex

Definitions	t  T, x:A. B(x), es-le(es; e; e'), prop{i:l}, P  Q, es-locl(es; e; e'), es-E(es), P  Q, False, P  Q, P  Q, P  Q, l_before(x; y; l; T), before(e), (x  l), append(as; bs), es-ble{i:l}(es;e;e'), b, filter(P; l), [e, e'], event_system{i:l}, guard(T), trans(T; x,y.E(x;y))
Lemmas	es-le-trans, event system wf, l before filter, filter wf, assert-es-ble, assert wf, es-ble wf, l before append iff, append wf, member singleton, l before-es-before-iff, member-es-before, l member wf, es-before wf, iff functionality wrt iff, and functionality wrt iff, or functionality wrt iff, singleton before, l before wf, false wf, es-E wf, es-locl wf, es-le wf